poss:(ES{i}Prop{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}),
P:(possible-event{i:l}(poss)Prop{i'}), e:possible-event{i:l}(poss).
es-knows{i:l}(poss; R; P; e)  Prop{i'} 

latex

Definitions	t  T, f(a), x:AB(x), Prop, P  Q, x:A. B(x), PossibleEvent(poss), K(P)@e, Type, ES
Lemmas	event system wf, possible-event wf